Formal analysis for robust anti-SPIT protection using model checking
Identifieur interne : 000061 ( Main/Exploration ); précédent : 000060; suivant : 000062Formal analysis for robust anti-SPIT protection using model checking
Auteurs : Dimitris Gritzalis [Grèce] ; Panagiotis Katsaros [Grèce] ; Stylianos Basagiannis [Grèce] ; Yannis Soupionis [Grèce]Source :
- International Journal of Information Security [ 1615-5262 ] ; 2012-04-01.
English descriptors
Abstract
Abstract: Anti-SPIT policies counter the SPam over Internet Telephony (SPIT) by distinguishing bots launching unsolicited bulks of VoIP calls from human beings. We propose an Anti-SPIT Policy Management mechanism (aSPM) that detects spam calls and prevents VoIP session establishment by the Session Initiation Protocol (SIP). The SPIN model checker is used to formally model and analyze the robustness of the aSPM mechanism in execution scenarios with parallel SIP sessions. In case of a possible design flaw, the model checker provides a trace of the caught unexpected behavior (counterexample), that can be used for the revision of the mechanism’s design. Our SPIN model is parameterized, based on measurements from experiments with VoIP users. Non-determinism plays a key role in representing all possible anti-SPIT policy decisions, in terms of the SIP messages that may be exchanged. The model checking results provide evidence for the timeliness of the parallel SIP sessions, the absence of deadlocks or livelocks, and the fairness for the VoIP service users. These findings ensure robust anti-SPIT protection, meaning that the aSPM mechanism operates as expected, despite the occurrence of random SPIT calls and communication error messages. To the best of our knowledge, this is the first analysis for exhaustively searching security policy flaws, due to complex interactions between anti-SPIT measures and the SIP protocol services.
Url:
DOI: 10.1007/s10207-012-0159-4
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000233
- to stream Istex, to step Curation: 000233
- to stream Istex, to step Checkpoint: 000014
- to stream Main, to step Merge: 000061
- to stream Main, to step Curation: 000061
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Formal analysis for robust anti-SPIT protection using model checking</title><author><name sortKey="Gritzalis, Dimitris" sort="Gritzalis, Dimitris" uniqKey="Gritzalis D" first="Dimitris" last="Gritzalis">Dimitris Gritzalis</name></author><author><name sortKey="Katsaros, Panagiotis" sort="Katsaros, Panagiotis" uniqKey="Katsaros P" first="Panagiotis" last="Katsaros">Panagiotis Katsaros</name></author><author><name sortKey="Basagiannis, Stylianos" sort="Basagiannis, Stylianos" uniqKey="Basagiannis S" first="Stylianos" last="Basagiannis">Stylianos Basagiannis</name></author><author><name sortKey="Soupionis, Yannis" sort="Soupionis, Yannis" uniqKey="Soupionis Y" first="Yannis" last="Soupionis">Yannis Soupionis</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:B25A57002A7BE4BBB9F4DE934CE147BA6365546C</idno><date when="2012" year="2012">2012</date><idno type="doi">10.1007/s10207-012-0159-4</idno><idno type="url">https://api.istex.fr/document/B25A57002A7BE4BBB9F4DE934CE147BA6365546C/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">000233</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000233</idno><idno type="wicri:Area/Istex/Curation">000233</idno><idno type="wicri:Area/Istex/Checkpoint">000014</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000014</idno><idno type="wicri:doubleKey">1615-5262:2012:Gritzalis D:formal:analysis:for</idno><idno type="wicri:Area/Main/Merge">000061</idno><idno type="wicri:Area/Main/Curation">000061</idno><idno type="wicri:Area/Main/Exploration">000061</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Formal analysis for robust anti-SPIT protection using model checking</title><author><name sortKey="Gritzalis, Dimitris" sort="Gritzalis, Dimitris" uniqKey="Gritzalis D" first="Dimitris" last="Gritzalis">Dimitris Gritzalis</name><affiliation wicri:level="3"><country xml:lang="fr">Grèce</country><wicri:regionArea>Information Security and Critical Infrastructure Protection Research Laboratory, Department of Informatics, Athens University of Economics and Business (AUEB), 76 Patission Ave., 10434, Athens</wicri:regionArea><placeName><settlement type="city">Athènes</settlement><region nuts="2" type="region">Attique (région)</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Grèce</country></affiliation></author><author><name sortKey="Katsaros, Panagiotis" sort="Katsaros, Panagiotis" uniqKey="Katsaros P" first="Panagiotis" last="Katsaros">Panagiotis Katsaros</name><affiliation wicri:level="1"><country xml:lang="fr">Grèce</country><wicri:regionArea>Dependability and Security Group, Department of Informatics, Aristotle University of Thessaloniki (AUTh), 54124, Thessaloniki</wicri:regionArea><wicri:noRegion>Thessaloniki</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Grèce</country></affiliation></author><author><name sortKey="Basagiannis, Stylianos" sort="Basagiannis, Stylianos" uniqKey="Basagiannis S" first="Stylianos" last="Basagiannis">Stylianos Basagiannis</name><affiliation wicri:level="1"><country xml:lang="fr">Grèce</country><wicri:regionArea>Dependability and Security Group, Department of Informatics, Aristotle University of Thessaloniki (AUTh), 54124, Thessaloniki</wicri:regionArea><wicri:noRegion>Thessaloniki</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Grèce</country></affiliation></author><author><name sortKey="Soupionis, Yannis" sort="Soupionis, Yannis" uniqKey="Soupionis Y" first="Yannis" last="Soupionis">Yannis Soupionis</name><affiliation wicri:level="3"><country xml:lang="fr">Grèce</country><wicri:regionArea>Information Security and Critical Infrastructure Protection Research Laboratory, Department of Informatics, Athens University of Economics and Business (AUEB), 76 Patission Ave., 10434, Athens</wicri:regionArea><placeName><settlement type="city">Athènes</settlement><region nuts="2" type="region">Attique (région)</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Grèce</country></affiliation></author></analytic><monogr></monogr><series><title level="j">International Journal of Information Security</title><title level="j" type="abbrev">Int. J. Inf. Secur.</title><idno type="ISSN">1615-5262</idno><idno type="eISSN">1615-5270</idno><imprint><publisher>Springer-Verlag</publisher><pubPlace>Berlin/Heidelberg</pubPlace><date type="published" when="2012-04-01">2012-04-01</date><biblScope unit="volume">11</biblScope><biblScope unit="issue">2</biblScope><biblScope unit="page" from="121">121</biblScope><biblScope unit="page" to="135">135</biblScope></imprint><idno type="ISSN">1615-5262</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">1615-5262</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Anti-SPIT security policies</term><term>Model checking</term><term>Robustness analysis</term><term>Voice over IP (VoIP)</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Anti-SPIT policies counter the SPam over Internet Telephony (SPIT) by distinguishing bots launching unsolicited bulks of VoIP calls from human beings. We propose an Anti-SPIT Policy Management mechanism (aSPM) that detects spam calls and prevents VoIP session establishment by the Session Initiation Protocol (SIP). The SPIN model checker is used to formally model and analyze the robustness of the aSPM mechanism in execution scenarios with parallel SIP sessions. In case of a possible design flaw, the model checker provides a trace of the caught unexpected behavior (counterexample), that can be used for the revision of the mechanism’s design. Our SPIN model is parameterized, based on measurements from experiments with VoIP users. Non-determinism plays a key role in representing all possible anti-SPIT policy decisions, in terms of the SIP messages that may be exchanged. The model checking results provide evidence for the timeliness of the parallel SIP sessions, the absence of deadlocks or livelocks, and the fairness for the VoIP service users. These findings ensure robust anti-SPIT protection, meaning that the aSPM mechanism operates as expected, despite the occurrence of random SPIT calls and communication error messages. To the best of our knowledge, this is the first analysis for exhaustively searching security policy flaws, due to complex interactions between anti-SPIT measures and the SIP protocol services.</div></front></TEI><affiliations><list><country><li>Grèce</li></country><region><li>Attique (région)</li></region><settlement><li>Athènes</li></settlement></list><tree><country name="Grèce"><region name="Attique (région)"><name sortKey="Gritzalis, Dimitris" sort="Gritzalis, Dimitris" uniqKey="Gritzalis D" first="Dimitris" last="Gritzalis">Dimitris Gritzalis</name></region><name sortKey="Basagiannis, Stylianos" sort="Basagiannis, Stylianos" uniqKey="Basagiannis S" first="Stylianos" last="Basagiannis">Stylianos Basagiannis</name><name sortKey="Basagiannis, Stylianos" sort="Basagiannis, Stylianos" uniqKey="Basagiannis S" first="Stylianos" last="Basagiannis">Stylianos Basagiannis</name><name sortKey="Gritzalis, Dimitris" sort="Gritzalis, Dimitris" uniqKey="Gritzalis D" first="Dimitris" last="Gritzalis">Dimitris Gritzalis</name><name sortKey="Katsaros, Panagiotis" sort="Katsaros, Panagiotis" uniqKey="Katsaros P" first="Panagiotis" last="Katsaros">Panagiotis Katsaros</name><name sortKey="Katsaros, Panagiotis" sort="Katsaros, Panagiotis" uniqKey="Katsaros P" first="Panagiotis" last="Katsaros">Panagiotis Katsaros</name><name sortKey="Soupionis, Yannis" sort="Soupionis, Yannis" uniqKey="Soupionis Y" first="Yannis" last="Soupionis">Yannis Soupionis</name><name sortKey="Soupionis, Yannis" sort="Soupionis, Yannis" uniqKey="Soupionis Y" first="Yannis" last="Soupionis">Yannis Soupionis</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Musique/explor/XenakisV1/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000061 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000061 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Musique
|area= XenakisV1
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:B25A57002A7BE4BBB9F4DE934CE147BA6365546C
|texte= Formal analysis for robust anti-SPIT protection using model checking
}}
| This area was generated with Dilib version V0.6.33. |  |